es:ES, ff:FIFO, f2f+:F2F+-decls, e:E, sndr, rcvr:ff.C.
[e: rcvr is_ack  sndr]  (loc(e) = rcvr  Id) 

latex

Definitions	t  T, P  Q, x:A. B(x), A c B, P & Q, [e: i p j],
Lemmas	f2f+-property, event system wf, FIFO wf, F2F+-decls wf, es-E wf, fifoC wf, f2f+Ack wf, snd-it wf